(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
    License: BSD
*)

section ‹Additions to the library›

theory Library_Complements
  imports "HOL-Analysis.Analysis" "HOL-Cardinals.Cardinal_Order_Relation"
begin

subsection ‹Mono intros›

text ‹We have a lot of (large) inequalities to prove. It is very convenient to have a set of
introduction rules for this purpose (a lot should be added to it, I have put here all the ones
I needed).

The typical use case is when one wants to prove some inequality, say
$ \exp (x*x) \leq y + \exp(1 + z * z + y)$, assuming $y \geq 0$ and $0 \leq x \leq z$.
One would write it has
\begin{verbatim}
have "0 + \exp(0 + x * x + 0) < = y + \exp(1 + z * z + y)"
using `y > = 0` `x < = z` by (intro mono_intros)
\end{verbatim}
When the left and right hand terms are written in completely analogous ways as above, then the
introduction rules (that contain monotonicity of addition, of the exponential, and so on) reduce
this to comparison of elementary terms in the formula. This is a very naive strategy, that fails
in many situations, but that is very efficient when used correctly.
›

named_theorems mono_intros "structural introduction rules to prove inequalities"
declare le_imp_neg_le [mono_intros]
declare add_left_mono [mono_intros]
declare add_right_mono [mono_intros]
declare add_strict_left_mono [mono_intros]
declare add_strict_right_mono [mono_intros]
declare add_mono [mono_intros]
declare add_less_le_mono [mono_intros]
declare diff_right_mono [mono_intros]
declare diff_left_mono [mono_intros]
declare diff_mono [mono_intros]
declare mult_left_mono [mono_intros]
declare mult_right_mono [mono_intros]
declare mult_mono [mono_intros]
declare max.mono [mono_intros]
declare min.mono [mono_intros]
declare power_mono [mono_intros]
declare ln_ge_zero [mono_intros]
declare ln_le_minus_one [mono_intros]
declare ennreal_minus_mono [mono_intros]
declare ennreal_leI [mono_intros]
declare e2ennreal_mono [mono_intros]
declare enn2ereal_nonneg [mono_intros]
declare zero_le [mono_intros]
declare top_greatest [mono_intros]
declare bot_least [mono_intros]
declare dist_triangle [mono_intros]
declare dist_triangle2 [mono_intros]
declare dist_triangle3 [mono_intros]
declare exp_ge_add_one_self [mono_intros]
declare exp_gt_one [mono_intros]
declare exp_less_mono [mono_intros]
declare dist_triangle [mono_intros]
declare abs_triangle_ineq [mono_intros]
declare abs_triangle_ineq2 [mono_intros]
declare abs_triangle_ineq2_sym [mono_intros]
declare abs_triangle_ineq3 [mono_intros]
declare abs_triangle_ineq4 [mono_intros]
declare Liminf_le_Limsup [mono_intros]
declare ereal_liminf_add_mono [mono_intros]
declare le_of_int_ceiling [mono_intros]
declare ereal_minus_mono [mono_intros]
declare infdist_triangle [mono_intros]
declare divide_right_mono [mono_intros]
declare self_le_power [mono_intros]

lemma ln_le_cancelI [mono_intros]:
  assumes "(0::real) < x" "x ≤ y"
  shows "ln x ≤ ln y"
using assms by auto

lemma exp_le_cancelI [mono_intros]:
  assumes "x ≤ (y::real)"
  shows "exp x ≤ exp y"
using assms by simp

lemma mult_ge1_mono [mono_intros]:
  assumes "a ≥ (0::'a::linordered_idom)" "b ≥ 1"
  shows "a ≤ a * b" "a ≤ b * a"
using assms mult_le_cancel_left1 mult_le_cancel_right1 by force+

text ‹A few convexity inequalities we will need later on.›

lemma xy_le_uxx_vyy [mono_intros]:
  assumes "u > 0" "u * v = (1::real)"
  shows "x * y ≤ u * x^2/2 + v * y^2/2"
proof -
  have "v > 0" using assms
    by (metis (full_types) dual_order.strict_implies_order le_less_linear mult_nonneg_nonpos not_one_le_zero)
  then have *: "sqrt u * sqrt v = 1"
    using assms by (metis real_sqrt_mult real_sqrt_one)
  have "(sqrt u * x - sqrt v * y)^2 ≥ 0" by auto
  then have "u * x^2 + v * y^2 - 2 * 1 * x * y ≥ 0"
    unfolding power2_eq_square *[symmetric] using ‹u > 0› ‹v > 0› by (auto simp add: algebra_simps)
  then show ?thesis by (auto simp add: algebra_simps divide_simps)
qed

lemma xy_le_xx_yy [mono_intros]:
  "x * y ≤ x^2/2 + y^2/2" for x y::real
using xy_le_uxx_vyy[of 1 1] by auto

lemma ln_squared_bound [mono_intros]:
  "(ln x)^2 ≤ 2 * x - 2" if "x ≥ 1" for x::real
proof -
  define f where "f = (λx::real. 2 * x - 2 - ln x * ln x)"
  have *: "DERIV f x :> 2 - 2 * ln x / x" if "x > 0" for x::real
    unfolding f_def using that by (auto intro!: derivative_eq_intros)
  have "f 1 ≤ f x" if "x ≥ 1" for x
  proof (rule DERIV_nonneg_imp_nondecreasing[OF that])
    fix t::real assume "t ≥ 1"
    show "∃y. (f has_real_derivative y) (at t) ∧ 0 ≤ y"
      apply (rule exI[of _ "2 - 2 * ln t / t"])
      using *[of t] ‹t ≥ 1› by (auto simp add: divide_simps ln_bound)
  qed
  then show ?thesis unfolding f_def power2_eq_square using that by auto
qed

text ‹In the next lemma, the assumptions are too strong (negative numbers
less than $-1$ also work well to have a square larger than $1$), but in practice one proves
inequalities with nonnegative numbers, so this version is really the useful one for
\verb+mono_intros+.›

lemma mult_ge1_powers [mono_intros]:
  assumes "a ≥ (1::'a::linordered_idom)"
  shows "1 ≤ a * a" "1 ≤ a * a * a" "1 ≤ a * a * a * a"
using assms by (meson assms dual_order.trans mult_ge1_mono(1) zero_le_one)+

lemmas [mono_intros] = ln_bound

lemma mono_cSup:
  fixes f :: "'a::conditionally_complete_lattice ⇒ 'b::conditionally_complete_lattice"
  assumes "bdd_above A" "A ≠ {}" "mono f"
  shows "Sup (f`A) ≤ f (Sup A)"
by (metis assms(1) assms(2) assms(3) cSUP_least cSup_upper mono_def)

lemma mono_cSup_bij:
  fixes f :: "'a::conditionally_complete_linorder ⇒ 'b::conditionally_complete_linorder"
  assumes "bdd_above A" "A ≠ {}" "mono f" "bij f"
  shows "Sup (f`A) = f(Sup A)"
proof -
  have "Sup ((inv f)`(f`A)) ≤ (inv f) (Sup (f`A))"
    apply (rule mono_cSup)
    using mono_inv[OF assms(3) assms(4)] assms(2) bdd_above_image_mono[OF assms(3) assms(1)] by auto
  then have "f (Sup ((inv f)`(f`A))) ≤ Sup (f`A)"
    using assms mono_def by (metis (no_types, hide_lams) bij_betw_imp_surj_on surj_f_inv_f)
  moreover have "f (Sup ((inv f)`(f`A))) = f(Sup A)"
    using assms by (simp add: bij_is_inj)
  ultimately show ?thesis using mono_cSup[OF assms(1) assms(2) assms(3)] by auto
qed

subsection ‹More topology›

text ‹In situations of interest to us later on, convergence is well controlled only for sequences
living in some dense subset of the space (but the limit can be anywhere). This is enough to
establish continuity of the function, if the target space is well enough separated.

The statement we give below is very general,
as we do not assume that the function is continuous inside the original set $S$, it will typically
only be continuous at a set $T$ contained in the closure of $S$. In many applications, $T$ will
be the closure of $S$, but we are also thinking of the case where one constructs an extension
of a function inside a space, to its boundary, and the behaviour at the boundary is better than
inside the space. The example we have in mind is the extension of a quasi-isometry to the boundary
of a Gromov hyperbolic space.

In the following criterion, we assume that if $u_n$ inside $S$ converges to a point at the boundary
$T$, then $f(u_n)$ converges (where $f$ is some function inside). Then, we can extend the function $f$ at
the boundary, by picking the limit value of $f(u_n)$ for some sequence converging to $u_n$. Then
the lemma asserts that $f$ is continuous at every point $b$ on the boundary.

The proof is done in two steps:
\begin{enumerate}
\item First, if $v_n$ is another inside sequence tending to
the same point $b$ on the boundary, then $f(v_n)$ converges to the same value as $f(u_n)$: this is
proved by considering the sequence $w$ equal to $u$ at even times and to $v$ at odd times, and
saying that $f(w_n)$ converges. Its limit is equal to the limit of $f(u_n)$ and of $f(v_n)$, so they
have to coincide.
\item Now, consider a general sequence $v$ (in the space or the boundary) converging to $b$. We want
to show that $f(v_n)$ tends to $f(b)$. If $v_n$ is inside $S$, we have already done it in the first
step. If it is on the boundary, on the other hand, we can approximate it by an inside point $w_n$
for which $f(w_n)$ is very close to $f(v_n)$. Then $w_n$ is an inside sequence converging to $b$,
hence $f(w_n)$ converges to $f(b)$ by the first step, and then $f(v_n)$ also converges to $f(b)$.
The precise argument is more conveniently written by contradiction. It requires good separation
properties of the target space.
\end{enumerate}›

text ‹First, we introduce the material to interpolate between two sequences, one at even times
and the other one at odd times.›

definition even_odd_interpolate::"(nat ⇒ 'a) ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ 'a)"
  where "even_odd_interpolate u v n = (if even n then u (n div 2) else v (n div 2))"

lemma even_odd_interpolate_compose:
  "even_odd_interpolate (f o u) (f o v) = f o (even_odd_interpolate u v)"
  unfolding even_odd_interpolate_def comp_def by auto

lemma even_odd_interpolate_filterlim:
  "filterlim u F sequentially ∧ filterlim v F sequentially ⟷ filterlim (even_odd_interpolate u v) F sequentially"
proof (auto)
  assume H: "filterlim (even_odd_interpolate u v) F sequentially"
  define r::"nat ⇒ nat" where "r = (λn. 2 * n)"
  have "strict_mono r" unfolding r_def strict_mono_def by auto
  then have "filterlim r sequentially sequentially"
    by (simp add: filterlim_subseq)
  have "filterlim (λn. (even_odd_interpolate u v) (r n)) F sequentially"
    by (rule filterlim_compose[OF H filterlim_subseq[OF ‹strict_mono r›]])
  moreover have "even_odd_interpolate u v (r n) = u n" for n
    unfolding r_def even_odd_interpolate_def by auto
  ultimately show "filterlim u F sequentially" by auto
  define r::"nat ⇒ nat" where "r = (λn. 2 * n + 1)"
  have "strict_mono r" unfolding r_def strict_mono_def by auto
  then have "filterlim r sequentially sequentially"
    by (simp add: filterlim_subseq)
  have "filterlim (λn. (even_odd_interpolate u v) (r n)) F sequentially"
    by (rule filterlim_compose[OF H filterlim_subseq[OF ‹strict_mono r›]])
  moreover have "even_odd_interpolate u v (r n) = v n" for n
    unfolding r_def even_odd_interpolate_def by auto
  ultimately show "filterlim v F sequentially" by auto
next
  assume H: "filterlim u F sequentially" "filterlim v F sequentially"
  show "filterlim (even_odd_interpolate u v) F sequentially"
  unfolding filterlim_iff eventually_sequentially proof (auto)
    fix P assume *: "eventually P F"
    obtain N1 where N1: "⋀n. n ≥ N1 ⟹ P (u n)"
      using H(1) unfolding filterlim_iff eventually_sequentially using * by auto
    obtain N2 where N2: "⋀n. n ≥ N2 ⟹ P (v n)"
      using H(2) unfolding filterlim_iff eventually_sequentially using * by auto
    have "P (even_odd_interpolate u v n)" if "n ≥ 2 * N1 + 2 * N2" for n
    proof (cases "even n")
      case True
      have "n div 2 ≥ N1" using that by auto
      then show ?thesis unfolding even_odd_interpolate_def using True N1 by auto
    next
      case False
      have "n div 2 ≥ N2" using that by auto
      then show ?thesis unfolding even_odd_interpolate_def using False N2 by auto
    qed
    then show "∃N. ∀n ≥ N. P (even_odd_interpolate u v n)" by auto
  qed
qed

text ‹Then, we prove the continuity criterion for extensions of functions to the boundary $T$ of a set
$S$. The first assumption is that $f(u_n)$ converges when $f$ converges to the boundary, and the
second one that the extension of $f$ to the boundary has been defined using the limit along some
sequence tending to the point under consideration. The following criterion is the most general one,
but this is not the version that is most commonly applied so we use a prime in its name.›

lemma continuous_at_extension_sequentially':
  fixes f :: "'a::{first_countable_topology, t2_space} ⇒ 'b::t3_space"
  assumes "b ∈ T"
          "⋀u b. (∀n. u n ∈ S) ⟹ b ∈ T ⟹ u ⇢ b ⟹ convergent (λn. f (u n))"
          "⋀b. b ∈ T ⟹ ∃u. (∀n. u n ∈ S) ∧ u ⇢ b ∧ ((λn. f (u n)) ⇢ f b)"
  shows "continuous (at b within (S ∪ T)) f"
proof -
  have first_step: "(λn. f (u n)) ⇢ f c" if "⋀n. u n ∈ S" "u ⇢ c" "c ∈ T" for u c
  proof -
    obtain v where v: "⋀n. v n ∈ S" "v ⇢ c" "(λn. f (v n)) ⇢ f c"
      using assms(3)[OF ‹c ∈ T›] by blast
    then have A: "even_odd_interpolate u v ⇢ c"
      unfolding even_odd_interpolate_filterlim[symmetric] using ‹u ⇢ c› by auto
    moreover have B: "∀n. even_odd_interpolate u v n ∈ S"
      using ‹⋀n. u n ∈ S› ‹⋀n. v n ∈ S› unfolding even_odd_interpolate_def by auto
    have "convergent (λn. f (even_odd_interpolate u v n))"
      by (rule assms(2)[OF B ‹c ∈ T› A])
    then obtain m where "(λn. f (even_odd_interpolate u v n)) ⇢ m"
      unfolding convergent_def by auto
    then have "even_odd_interpolate (f o u) (f o v) ⇢ m"
      unfolding even_odd_interpolate_compose unfolding comp_def by auto
    then have "(f o u) ⇢ m" "(f o v) ⇢ m"
      unfolding even_odd_interpolate_filterlim[symmetric] by auto
    then have "m = f c" using v(3) unfolding comp_def using LIMSEQ_unique by auto
    then show ?thesis using ‹(f o u) ⇢ m› unfolding comp_def by auto
  qed
  show "continuous (at b within (S ∪ T)) f"
  proof (rule ccontr)
    assume "¬ ?thesis"
    then obtain U where U: "open U" "f b ∈ U" "¬(∀⇩F x in at b within S ∪ T. f x ∈ U)"
      unfolding continuous_within tendsto_def[where l = "f b"] using sequentially_imp_eventually_nhds_within by auto
    have "∃V W. open V ∧ open W ∧ f b ∈ V ∧ (UNIV - U) ⊆ W ∧ V ∩ W = {}"
      apply (rule t3_space) using U by auto
    then obtain V W where VW: "open V" "open W" "f b ∈ V" "UNIV - U ⊆ W" "V ∩ W = {}"
      by auto

    obtain A :: "nat ⇒ 'a set" where *:
      "⋀i. open (A i)"
      "⋀i. b ∈ A i"
      "⋀F. ∀n. F n ∈ A n ⟹ F ⇢ b"
      by (rule first_countable_topology_class.countable_basis) blast
    with * U(3) have "∃F. ∀n. F n ∈ S ∪ T ∧ F n ∈ A n ∧ ¬ (f(F n) ∈ U)"
      unfolding at_within_def eventually_inf_principal eventually_nhds
      by (intro choice) (meson DiffE)
    then obtain F where F: "⋀n. F n ∈ S ∪ T" "⋀n. F n ∈ A n" "⋀n. f(F n) ∉ U"
      by auto

    have "∃y. y ∈ S ∧ y ∈ A n ∧ f y ∈ W" for n
    proof (cases "F n ∈ S")
      case True
      show ?thesis apply (rule exI[of _ "F n"]) using F VW True by auto
    next
      case False
      then have "F n ∈ T" using ‹F n ∈ S ∪ T› by auto
      obtain u where u: "⋀p. u p ∈ S" "u ⇢ F n" "(λp. f (u p)) ⇢ f(F n)"
        using assms(3)[OF ‹F n ∈ T›] by auto
      moreover have "f(F n) ∈ W" using F VW by auto
      ultimately have "eventually (λp. f (u p) ∈ W) sequentially"
        using ‹open W› by (simp add: tendsto_def)
      moreover have "eventually (λp. u p ∈ A n) sequentially"
        using ‹F n ∈ A n› u ‹open (A n)› by (simp add: tendsto_def)
      ultimately have "∃p. f(u p) ∈ W ∧ u p ∈ A n"
        using eventually_False_sequentially eventually_elim2 by blast
      then show ?thesis using u(1) by auto
    qed
    then have "∃u. ∀n. u n ∈ S ∧ u n ∈ A n ∧ f (u n) ∈ W"
      by (auto intro: choice)
    then obtain u where u: "⋀n. u n ∈ S" "⋀n. u n ∈ A n" "⋀n. f (u n) ∈ W"
      by blast
    then have "u ⇢ b" using *(3) by auto
    then have "(λn. f (u n)) ⇢ f b" using first_step assms u by auto
    then have "eventually (λn. f (u n) ∈ V) sequentially"
      using VW by (simp add: tendsto_def)
    then have "∃n. f (u n) ∈ V"
      using eventually_False_sequentially eventually_elim2 by blast
    then show False
      using u(3) ‹V ∩ W = {}› by auto
  qed
qed

text ‹We can specialize the previous statement to the common case where one already knows the
sequential continuity of $f$ along sequences in $S$ converging to a point in $T$. This will be the
case in most --but not all-- applications. This is a straightforward application of the above
criterion.›

proposition continuous_at_extension_sequentially:
  fixes f :: "'a::{first_countable_topology, t2_space} ⇒ 'b::t3_space"
  assumes "a ∈ T"
          "T ⊆ closure S"
          "⋀u b. (∀n. u n ∈ S) ⟹ b ∈ T ⟹ u ⇢ b ⟹ (λn. f (u n)) ⇢ f b"
  shows "continuous (at a within (S ∪ T)) f"
apply (rule continuous_at_extension_sequentially'[OF ‹a ∈ T›])
using assms(3) convergent_def apply blast
by (metis assms(2) assms(3) closure_sequential subset_iff)

text ‹We also give global versions. We can only express the continuity on $T$, so
this is slightly weaker than the previous statements since we are not saying anything on inside
sequences tending to $T$ -- but in cases where $T$ contains $S$ these statements contain all the
information.›

lemma continuous_on_extension_sequentially':
  fixes f :: "'a::{first_countable_topology, t2_space} ⇒ 'b::t3_space"
  assumes "⋀u b. (∀n. u n ∈ S) ⟹ b ∈ T ⟹ u ⇢ b ⟹ convergent (λn. f (u n))"
          "⋀b. b ∈ T ⟹ ∃u. (∀n. u n ∈ S) ∧ u ⇢ b ∧ ((λn. f (u n)) ⇢ f b)"
  shows "continuous_on T f"
unfolding continuous_on_eq_continuous_within apply (auto intro!: continuous_within_subset[of _ "S ∪ T" f T])
by (intro continuous_at_extension_sequentially'[OF _ assms], auto)

lemma continuous_on_extension_sequentially:
  fixes f :: "'a::{first_countable_topology, t2_space} ⇒ 'b::t3_space"
  assumes "T ⊆ closure S"
          "⋀u b. (∀n. u n ∈ S) ⟹ b ∈ T ⟹ u ⇢ b ⟹ (λn. f (u n)) ⇢ f b"
  shows "continuous_on T f"
unfolding continuous_on_eq_continuous_within apply (auto intro!: continuous_within_subset[of _ "S ∪ T" f T])
by (intro continuous_at_extension_sequentially[OF _ assms], auto)


subsubsection ‹Homeomorphisms›

text ‹A variant around the notion of homeomorphism, which is only expressed in terms of the
function and not of its inverse.›

definition homeomorphism_on::"'a set ⇒ ('a::topological_space ⇒ 'b::topological_space) ⇒ bool"
  where "homeomorphism_on S f = (∃g. homeomorphism S (f`S) f g)"

lemma homeomorphism_on_continuous:
  assumes "homeomorphism_on S f"
  shows "continuous_on S f"
using assms unfolding homeomorphism_on_def homeomorphism_def by auto

lemma homeomorphism_on_bij:
  assumes "homeomorphism_on S f"
  shows "bij_betw f S (f`S)"
using assms unfolding homeomorphism_on_def homeomorphism_def by auto (metis inj_on_def inj_on_imp_bij_betw)

lemma homeomorphism_on_homeomorphic:
  assumes "homeomorphism_on S f"
  shows "S homeomorphic (f`S)"
using assms unfolding homeomorphism_on_def homeomorphic_def by auto

lemma homeomorphism_on_compact:
  fixes f::"'a::topological_space ⇒ 'b::t2_space"
  assumes "continuous_on S f"
          "compact S"
          "inj_on f S"
  shows "homeomorphism_on S f"
unfolding homeomorphism_on_def using homeomorphism_compact[OF assms(2) assms(1) _ assms(3)] by auto

lemma homeomorphism_on_subset:
  assumes "homeomorphism_on S f"
          "T ⊆ S"
  shows "homeomorphism_on T f"
using assms homeomorphism_of_subsets unfolding homeomorphism_on_def by blast

lemma homeomorphism_on_empty [simp]:
  "homeomorphism_on {} f"
unfolding homeomorphism_on_def using homeomorphism_empty[of f] by auto

lemma homeomorphism_on_cong:
  assumes "homeomorphism_on X f"
          "X' = X" "⋀x. x ∈ X ⟹ f' x = f x"
  shows "homeomorphism_on X' f'"
proof -
  obtain g where g:"homeomorphism X (f`X) f g"
    using assms unfolding homeomorphism_on_def by auto
  have "homeomorphism X' (f'`X') f' g"
    apply (rule homeomorphism_cong[OF g]) using assms by (auto simp add: rev_image_eqI)
  then show ?thesis
    unfolding homeomorphism_on_def by auto
qed

lemma homeomorphism_on_inverse:
  fixes f::"'a::topological_space ⇒ 'b::topological_space"
  assumes "homeomorphism_on X f"
  shows "homeomorphism_on (f`X) (inv_into X f)"
proof -
  obtain g where g: "homeomorphism X (f`X) f g"
    using assms unfolding homeomorphism_on_def by auto
  then have "g`f`X = X"
    by (simp add: homeomorphism_def)
  then have "homeomorphism_on (f`X) g"
    unfolding homeomorphism_on_def using homeomorphism_symD[OF g] by auto
  moreover have "g x = inv_into X f x" if "x ∈ f`X" for x
    using g that unfolding homeomorphism_def by (auto, metis f_inv_into_f inv_into_into that)
  ultimately show ?thesis
    using homeomorphism_on_cong by force
qed

text ‹Characterization of homeomorphisms in terms of sequences: a map is a homeomorphism if and
only if it respects convergent sequences.›

lemma homeomorphism_on_compose:
  assumes "homeomorphism_on S f"
          "x ∈ S"
          "eventually (λn. u n ∈ S) F"
  shows "(u ⤏ x) F ⟷ ((λn. f (u n)) ⤏ f x) F"
proof
  assume "(u ⤏ x) F"
  then show "((λn. f (u n)) ⤏ f x) F"
    using continuous_on_tendsto_compose[OF homeomorphism_on_continuous[OF assms(1)] _ assms(2) assms(3)] by simp
next
  assume *: "((λn. f (u n)) ⤏ f x) F"
  have I: "inv_into S f (f y) = y" if "y ∈ S" for y
    using homeomorphism_on_bij[OF assms(1)] by (meson bij_betw_inv_into_left that)
  then have A: "eventually (λn. u n = inv_into S f (f (u n))) F"
    using assms eventually_mono by force
  have "((λn. (inv_into S f) (f (u n))) ⤏ (inv_into S f) (f x)) F"
    apply (rule continuous_on_tendsto_compose[OF homeomorphism_on_continuous[OF homeomorphism_on_inverse[OF assms(1)]] *])
    using assms eventually_mono by (auto) fastforce
  then show "(u ⤏ x) F"
    unfolding tendsto_cong[OF A] I[OF ‹x ∈ S›] by simp
qed

lemma homeomorphism_on_sequentially:
  fixes f::"'a::{first_countable_topology, t2_space} ⇒ 'b::{first_countable_topology, t2_space}"
  assumes "⋀x u. x ∈ S ⟹ (∀n. u n ∈ S) ⟹ u ⇢ x ⟷ (λn. f (u n)) ⇢ f x"
  shows "homeomorphism_on S f"
proof -
  have "x = y" if "f x = f y" "x ∈ S" "y ∈ S" for x y
  proof -
    have "(λn. f x) ⇢ f y" using that by auto
    then have "(λn. x) ⇢ y" using assms(1) that by auto
    then show "x = y" using LIMSEQ_unique by auto
  qed
  then have "inj_on f S" by (simp add: inj_on_def)

  have Cf: "continuous_on S f"
    apply (rule continuous_on_sequentiallyI) using assms by auto
  define g where "g = inv_into S f"
  have Cg: "continuous_on (f`S) g"
  proof (rule continuous_on_sequentiallyI)
    fix v b assume H: "∀n. v n ∈ f ` S" "b ∈ f ` S" "v ⇢ b"
    define u where "u = (λn. g (v n))"
    define a where "a = g b"
    have "u n ∈ S" "f (u n) = v n" for n
      unfolding u_def g_def using H(1) by (auto simp add: inv_into_into f_inv_into_f)
    have "a ∈ S" "f a = b"
      unfolding a_def g_def using H(2) by (auto simp add: inv_into_into f_inv_into_f)
    show "(λn. g(v n)) ⇢ g b"
      unfolding u_def[symmetric] a_def[symmetric] apply (rule iffD2[OF assms])
      using ‹⋀n. u n ∈ S› ‹a ∈ S› ‹v ⇢ b›
      unfolding ‹⋀n. f (u n) = v n› ‹f a = b› by auto
  qed
  have "homeomorphism S (f`S) f g"
    apply (rule homeomorphismI[OF Cf Cg]) unfolding g_def using ‹inj_on f S› by auto
  then show ?thesis
    unfolding homeomorphism_on_def by auto
qed

lemma homeomorphism_on_UNIV_sequentially:
  fixes f::"'a::{first_countable_topology, t2_space} ⇒ 'b::{first_countable_topology, t2_space}"
  assumes "⋀x u. u ⇢ x ⟷ (λn. f (u n)) ⇢ f x"
  shows "homeomorphism_on UNIV f"
using assms by (auto intro!: homeomorphism_on_sequentially)

text ‹Now, we give similar characterizations in terms of sequences living in a dense subset. As
in the sequential continuity criteria above, we first give a very general criterion, where the map
does not have to be continuous on the approximating set $S$, only on the limit set $T$, without
any a priori identification of the limit. Then, we specialize this statement to a less general
but often more usable version.›

lemma homeomorphism_on_extension_sequentially_precise:
  fixes f::"'a::{first_countable_topology, t3_space} ⇒ 'b::{first_countable_topology, t3_space}"
  assumes "⋀u b. (∀n. u n ∈ S) ⟹ b ∈ T ⟹ u ⇢ b ⟹ convergent (λn. f (u n))"
          "⋀u c. (∀n. u n ∈ S) ⟹ c ∈ f`T ⟹ (λn. f (u n)) ⇢ c ⟹ convergent u"
          "⋀b. b ∈ T ⟹ ∃u. (∀n. u n ∈ S) ∧ u ⇢ b ∧ ((λn. f (u n)) ⇢ f b)"
          "⋀n. u n ∈ S ∪ T" "l ∈ T"
  shows "u ⇢ l ⟷ (λn. f (u n)) ⇢ f l"
proof
  assume H: "u ⇢ l"
  have "continuous (at l within (S ∪ T)) f"
    apply (rule continuous_at_extension_sequentially'[OF ‹l ∈ T›]) using assms(1) assms(3) by auto
  then show "(λn. f (u n)) ⇢ f l"
    apply (rule continuous_within_tendsto_compose) using H assms(4) by auto
next
  text ‹For the reverse implication, we would like to use the continuity criterion
  \verb+ continuous_at_extension_sequentially'+ applied to the inverse of $f$. Unfortunately, this
  inverse is only well defined on $T$, while our sequence takes values in $S \cup T$. So, instead,
  we redo by hand the proof of the continuity criterion, but in the opposite direction.›
  assume H: "(λn. f (u n)) ⇢ f l"
  show "u ⇢ l"
  proof (rule ccontr)
    assume "¬ ?thesis"
    then obtain U where U: "open U" "l ∈ U" "¬(∀⇩F n in sequentially. u n ∈ U)"
      unfolding continuous_within tendsto_def[where l = l] using sequentially_imp_eventually_nhds_within by auto
    obtain A :: "nat ⇒ 'b set" where *:
      "⋀i. open (A i)"
      "⋀i. f l ∈ A i"
      "⋀F. ∀n. F n ∈ A n ⟹ F ⇢ f l"
      by (rule first_countable_topology_class.countable_basis) blast
    have B: "eventually (λn. f (u n) ∈ A i) sequentially" for i
      using ‹open (A i)› ‹f l ∈ A i› H topological_tendstoD by fastforce
    have M: "∃r. r ≥ N ∧ (u r ∉ U) ∧ f (u r) ∈ A i" for N i
      using U(3) B[of i] unfolding eventually_sequentially by (meson dual_order.trans le_cases)
    have "∃r. ∀n. (u (r n) ∉ U ∧ f (u (r n)) ∈ A n) ∧ r (Suc n) ≥ r n + 1"
      apply (rule dependent_nat_choice) using M by auto
    then obtain r where r: "⋀n. u (r n) ∉ U" "⋀n. f (u (r n)) ∈ A n" "⋀n. r (Suc n) ≥ r n + 1"
      by auto
    then have "strict_mono r"
      by (metis Suc_eq_plus1 Suc_le_lessD strict_monoI_Suc)

    have "∃V W. open V ∧ open W ∧ l ∈ V ∧ (UNIV - U) ⊆ W ∧ V ∩ W = {}"
      apply (rule t3_space) using U by auto
    then obtain V W where VW: "open V" "open W" "l ∈ V" "UNIV - U ⊆ W" "V ∩ W = {}"
      by auto

    have "∃z. z ∈ S ∧ f z ∈ A n ∧ z ∈ W" for n
    proof -
      define z where "z = u (r n)"
      have "f z ∈ A n" unfolding z_def using r(2) by auto
      have "z ∈ S ∪ T" "z ∉ U"
        unfolding z_def using r(1) assms(4) by auto
      then have "z ∈ W" using VW by auto
      show ?thesis
      proof (cases "z ∈ T")
        case True
        obtain u::"nat ⇒ 'a" where u: "⋀p. u p ∈ S" "u ⇢ z" "(λp. f (u p)) ⇢ f z"
          using assms(3)[OF ‹z ∈ T›] by auto
        then have "eventually (λp. f (u p) ∈ A n) sequentially"
          using ‹open (A n)› ‹f z ∈ A n› unfolding tendsto_def by simp
        moreover have "eventually (λp. u p ∈ W) sequentially"
          using ‹open W› ‹z ∈ W› u unfolding tendsto_def by simp
        ultimately have "∃p. u p ∈ W ∧ f (u p) ∈ A n"
          using eventually_False_sequentially eventually_elim2 by blast
        then show ?thesis using u(1) by auto
      next
        case False
        then have "z ∈ S" using ‹z ∈ S ∪ T› by auto
        then show ?thesis using ‹f z ∈ A n› ‹z ∈ W› by auto
      qed
    qed
    then have "∃v. ∀n. v n ∈ S ∧ f (v n) ∈ A n ∧ v n ∈ W"
      by (auto intro: choice)
    then obtain v where v: "⋀n. v n ∈ S" "⋀n. f (v n) ∈ A n" "⋀n. v n ∈ W"
      by blast
    then have I: "(λn. f (v n)) ⇢ f l" using *(3) by auto

    obtain w where w: "⋀n. w n ∈ S" "w ⇢ l" "((λn. f (w n)) ⇢ f l)"
      using assms(3)[OF ‹l ∈ T›] by auto
    have "even_odd_interpolate (f o v) (f o w) ⇢ f l"
      unfolding even_odd_interpolate_filterlim[symmetric] comp_def using v w I by auto
    then have *: "(λn. f (even_odd_interpolate v w n)) ⇢ f l"
      unfolding even_odd_interpolate_compose unfolding comp_def by auto
    have "convergent (even_odd_interpolate v w)"
      apply (rule assms(2)[OF _ _ *])
      unfolding even_odd_interpolate_def using v(1) w(1) ‹l ∈ T› by auto
    then obtain z where "even_odd_interpolate v w ⇢ z"
      unfolding convergent_def by auto
    then have *: "v ⇢ z" "w ⇢ z" unfolding even_odd_interpolate_filterlim[symmetric] by auto
    then have "z = l" using v(2) w(2) LIMSEQ_unique by auto
    then have "v ⇢ l" using * by simp
    then have "eventually (λn. v n ∈ V) sequentially"
      using VW by (simp add: tendsto_def)
    then have "∃n. v n ∈ V"
      using eventually_False_sequentially eventually_elim2 by blast
    then show False
      using v(3) ‹V ∩ W = {}› by auto
  qed
qed

lemma homeomorphism_on_extension_sequentially':
  fixes f::"'a::{first_countable_topology, t3_space} ⇒ 'b::{first_countable_topology, t3_space}"
  assumes "⋀u b. (∀n. u n ∈ S) ⟹ b ∈ T ⟹ u ⇢ b ⟹ convergent (λn. f (u n))"
          "⋀u c. (∀n. u n ∈ S) ⟹ c ∈ f`T ⟹ (λn. f (u n)) ⇢ c ⟹ convergent u"
          "⋀b. b ∈ T ⟹ ∃u. (∀n. u n ∈ S) ∧ u ⇢ b ∧ ((λn. f (u n)) ⇢ f b)"
  shows "homeomorphism_on T f"
apply (rule homeomorphism_on_sequentially, rule homeomorphism_on_extension_sequentially_precise[of S T])
using assms by auto

proposition homeomorphism_on_extension_sequentially:
  fixes f::"'a::{first_countable_topology, t3_space} ⇒ 'b::{first_countable_topology, t3_space}"
  assumes "⋀u b. (∀n. u n ∈ S) ⟹ u ⇢ b ⟷ (λn. f (u n)) ⇢ f b"
          "T ⊆ closure S"
  shows "homeomorphism_on T f"
apply (rule homeomorphism_on_extension_sequentially'[of S])
using assms(1) convergent_def apply fastforce
using assms(1) convergent_def apply blast
by (metis assms(1) assms(2) closure_sequential subsetCE)

lemma homeomorphism_on_UNIV_extension_sequentially:
  fixes f::"'a::{first_countable_topology, t3_space} ⇒ 'b::{first_countable_topology, t3_space}"
  assumes "⋀u b. (∀n. u n ∈ S) ⟹ u ⇢ b ⟷ (λn. f (u n)) ⇢ f b"
          "closure S = UNIV"
  shows "homeomorphism_on UNIV f"
apply (rule homeomorphism_on_extension_sequentially[of S]) using assms by auto


subsubsection ‹Proper spaces›

text ‹Proper spaces, i.e., spaces in which every closed ball is compact -- or, equivalently,
any closed bounded set is compact.›

definition proper::"('a::metric_space) set ⇒ bool"
  where "proper S ≡ (∀ x r. compact (cball x r ∩ S))"

lemma properI:
  assumes "⋀x r. compact (cball x r ∩ S)"
  shows "proper S"
using assms unfolding proper_def by auto

lemma proper_compact_cball:
  assumes "proper (UNIV::'a::metric_space set)"
  shows "compact (cball (x::'a) r)"
using assms unfolding proper_def by auto

lemma proper_compact_bounded_closed:
  assumes "proper (UNIV::'a::metric_space set)" "closed (S::'a set)" "bounded S"
  shows "compact S"
proof -
  obtain x r where "S ⊆ cball x r"
    using ‹bounded S› bounded_subset_cball by blast
  then have *: "S = S ∩ cball x r"
    by auto
  show ?thesis
    apply (subst *, rule closed_Int_compact) using assms unfolding proper_def by auto
qed

lemma proper_real [simp]:
  "proper (UNIV::real set)"
unfolding proper_def by auto

lemma complete_of_proper:
  assumes "proper S"
  shows "complete S"
proof -
  have "∃l∈S. u ⇢ l" if "Cauchy u" "⋀n. u n ∈ S" for u
  proof -
    have "bounded (range u)"
      using ‹Cauchy u› cauchy_imp_bounded by auto
    then obtain x r where *: "⋀n. dist x (u n) ≤ r"
      unfolding bounded_def by auto
    then have "u n ∈ (cball x r) ∩ S" for n using ‹u n ∈ S› by auto
    moreover have "complete ((cball x r) ∩ S)"
      apply (rule compact_imp_complete) using assms unfolding proper_def by auto
    ultimately show ?thesis
      unfolding complete_def using ‹Cauchy u› by auto
  qed
  then show ?thesis
    unfolding complete_def by auto
qed

lemma proper_of_compact:
  assumes "compact S"
  shows "proper S"
using assms by (auto intro: properI)

lemma proper_Un:
  assumes "proper A" "proper B"
  shows "proper (A ∪ B)"
using assms unfolding proper_def by (auto simp add: compact_Un inf_sup_distrib1)

subsubsection ‹Miscellaneous topology›

text ‹When manipulating the triangle inequality, it is very frequent to deal with 4 points
(and automation has trouble doing it automatically). Even sometimes with 5 points...›

lemma dist_triangle4 [mono_intros]:
  "dist x t ≤ dist x y + dist y z + dist z t"
using dist_triangle[of x z y] dist_triangle[of x t z] by auto

lemma dist_triangle5 [mono_intros]:
  "dist x u ≤ dist x y + dist y z + dist z t + dist t u"
using dist_triangle4[of x u y z] dist_triangle[of z u t] by auto

text ‹A thickening of a compact set is closed.›

lemma compact_has_closed_thickening:
  assumes "compact C"
          "continuous_on C f"
  shows "closed (⋃x∈C. cball x (f x))"
proof (auto simp add: closed_sequential_limits)
  fix u l assume *: "∀n::nat. ∃x∈C. dist x (u n) ≤ f x" "u ⇢ l"
  have "∃x::nat⇒'a. ∀n. x n ∈ C ∧ dist (x n) (u n) ≤ f (x n)"
    apply (rule choice) using * by auto
  then obtain x::"nat ⇒ 'a" where x: "⋀n. x n ∈ C" "⋀n. dist (x n) (u n) ≤ f (x n)"
    by blast
  obtain r c where "strict_mono r" "c ∈ C" "(x o r) ⇢ c"
    using x(1) ‹compact C› by (meson compact_eq_seq_compact_metric seq_compact_def)
  then have "c ∈ C" using x(1) ‹compact C› by auto
  have lim: "(λn. f (x (r n)) - dist (x (r n)) (u (r n))) ⇢ f c - dist c l"
    apply (intro tendsto_intros, rule continuous_on_tendsto_compose[of C f])
    using *(2) x(1) ‹(x o r) ⇢ c› ‹continuous_on C f› ‹c ∈ C› ‹strict_mono r› LIMSEQ_subseq_LIMSEQ
    unfolding comp_def by auto
  have "f c - dist c l ≥ 0" apply (rule LIMSEQ_le_const[OF lim]) using x(2) by auto
  then show "∃x∈C. dist x l ≤ f x" using ‹c ∈ C› by auto
qed

text ‹congruence rule for continuity. The assumption that $f y = g y$ is necessary since \verb+at x+
is the pointed neighborhood at $x$.›

lemma continuous_within_cong:
  assumes "continuous (at y within S) f"
          "eventually (λx. f x = g x) (at y within S)"
          "f y = g y"
  shows "continuous (at y within S) g"
  using assms continuous_within filterlim_cong by fastforce

text ‹A function which tends to infinity at infinity, on a proper set, realizes its infimum›

lemma continuous_attains_inf_proper:
  fixes f :: "'a::metric_space ⇒ 'b::linorder_topology"
  assumes "proper s" "a ∈ s"
          "continuous_on s f"
          "⋀z. z ∈ s - cball a r ⟹ f z ≥ f a"
  shows "∃x∈s. ∀y∈s. f x ≤ f y"
proof (cases "r ≥ 0")
  case True
  have "∃x∈cball a r ∩ s. ∀y ∈ cball a r ∩ s. f x ≤ f y"
    apply (rule continuous_attains_inf) using assms True unfolding proper_def apply (auto simp add: continuous_on_subset)
    using centre_in_cball by blast
  then obtain x where x: "x ∈ cball a r ∩ s" "⋀y. y ∈ cball a r ∩ s ⟹ f x ≤ f y"
    by auto
  have "f x ≤ f y" if "y ∈ s" for y
  proof (cases "y ∈ cball a r")
    case True
    then show ?thesis using x(2) that by auto
  next
    case False
    have "f x ≤ f a"
      apply (rule x(2)) using assms True by auto
    then show ?thesis using assms(4)[of y] that False by auto
  qed
  then show ?thesis using x(1) by auto
next
  case False
  show ?thesis
    apply (rule bexI[of _ a]) using assms False by auto
qed

subsubsection ‹Measure of balls›

text ‹The image of a ball by an affine map is still a ball, with explicit center and radius. (Now unused)›

lemma affine_image_ball [simp]:
  "(λy. R *⇩R y + x) ` cball 0 1 = cball (x::('a::real_normed_vector)) ¦R¦"
proof
  have "dist x (R *⇩R y + x) ≤ ¦R¦" if "dist 0 y ≤ 1" for y
  proof -
    have "dist x (R *⇩R y + x) = norm ((R *⇩R y + x) - x)" by (simp add: dist_norm)
    also have "... = ¦R¦ * norm y" by auto
    finally show ?thesis using that by (simp add: mult_left_le)
  qed
  then show "(λy. R *⇩R y + x) ` cball 0 1 ⊆ cball x ¦R¦" by auto

  show "cball x ¦R¦ ⊆ (λy. R *⇩R y + x) ` cball 0 1"
  proof (cases "¦R¦ = 0")
    case True
    then have "cball x ¦R¦ = {x}" by auto
    moreover have "x = R *⇩R 0 + x ∧ 0 ∈ cball 0 1" by auto
    ultimately show ?thesis by auto
  next
    case False
    have "z ∈ (λy. R *⇩R y + x) ` cball 0 1" if "z ∈ cball x ¦R¦" for z
    proof -
      define y where "y = (z - x) /⇩R R"
      have "R *⇩R y + x = z" unfolding y_def using False by auto
      moreover have "y ∈ cball 0 1"
        using ‹z ∈ cball x ¦R¦› False unfolding y_def by (auto simp add: dist_norm[symmetric] divide_simps dist_commute)
      ultimately show ?thesis by auto
    qed
    then show ?thesis by auto
  qed
qed

text ‹From the rescaling properties of Lebesgue measure in a euclidean space, it follows that
the measure of any ball can be expressed in terms of the measure of the unit ball.›

lemma lebesgue_measure_ball:
  assumes "R ≥ 0"
  shows "measure lborel (cball (x::('a::euclidean_space)) R) = R^(DIM('a)) * measure lborel (cball (0::'a) 1)"
        "emeasure lborel (cball (x::('a::euclidean_space)) R) = R^(DIM('a)) * emeasure lborel (cball (0::'a) 1)"
  apply (simp add: assms content_cball)
  by (simp add: assms emeasure_cball ennreal_mult' ennreal_power mult.commute)

text ‹We show that the unit ball has positive measure -- this is obvious, but useful. We could
show it by arguing that it contains a box, whose measure can be computed, but instead we say
that if the measure vanished then the measure of any ball would also vanish, contradicting the
fact that the space has infinite measure. This avoids all computations.›

lemma lebesgue_measure_ball_pos:
  "emeasure lborel (cball (0::'a::euclidean_space) 1) > 0"
  "measure lborel (cball (0::'a::euclidean_space) 1) > 0"
proof -
  show "emeasure lborel (cball (0::'a::euclidean_space) 1) > 0"
  proof (rule ccontr)
    assume "¬(emeasure lborel (cball (0::'a::euclidean_space) 1) > 0)"
    then have "emeasure lborel (cball (0::'a) 1) = 0" by auto
    then have "emeasure lborel (cball (0::'a) n) = 0" for n::nat
      using lebesgue_measure_ball(2)[of "real n" 0] by (metis mult_zero_right of_nat_0_le_iff)
    then have "emeasure lborel (⋃n. cball (0::'a) (real n)) = 0"
      by (metis (mono_tags, lifting) borel_closed closed_cball emeasure_UN_eq_0 imageE sets_lborel subsetI)
    moreover have "(⋃n. cball (0::'a) (real n)) = UNIV" by (auto simp add: real_arch_simple)
    ultimately show False
      by simp
  qed
  moreover have "emeasure lborel (cball (0::'a::euclidean_space) 1) < ∞"
    by (rule emeasure_bounded_finite, auto)
  ultimately show "measure lborel (cball (0::'a::euclidean_space) 1) > 0"
    by (metis borel_closed closed_cball ennreal_0 has_integral_iff_emeasure_lborel has_integral_measure_lborel less_irrefl order_refl zero_less_measure_iff)
qed

subsubsection ‹infdist and closest point projection›

text ‹The distance to a union of two sets is the minimum of the distance to the two sets.›

lemma infdist_union_min [mono_intros]:
  assumes "A ≠ {}" "B ≠ {}"
  shows "infdist x (A ∪ B) = min (infdist x A) (infdist x B)"
using assms by (simp add: infdist_def cINF_union inf_real_def)

text ‹The distance to a set is non-increasing with the set.›

lemma infdist_mono [mono_intros]:
  assumes "A ⊆ B" "A ≠ {}"
  shows "infdist x B ≤ infdist x A"
  by (simp add: assms infdist_eq_setdist setdist_subset_right)

text ‹If a set is proper, then the infimum of the distances to this set is attained.›

lemma infdist_proper_attained:
  assumes "proper C" "C ≠ {}"
  shows "∃c∈C. infdist x C = dist x c"
proof -
  obtain a where "a ∈ C" using assms by auto
  have *: "dist x a ≤ dist x z" if "dist a z ≥ 2 * dist a x" for z
  proof -
    have "2 * dist a x ≤ dist a z" using that by simp
    also have "... ≤ dist a x + dist x z" by (intro mono_intros)
    finally show ?thesis by (simp add: dist_commute)
  qed
  have "∃c∈C. ∀d∈C. dist x c ≤ dist x d"
    apply (rule continuous_attains_inf_proper[OF assms(1) ‹a ∈ C›, of _ "2 * dist a x"])
    using * by (auto intro: continuous_intros)
  then show ?thesis unfolding infdist_def using ‹C ≠ {}›
    by (metis antisym bdd_below_image_dist cINF_lower le_cINF_iff)
qed

lemma infdist_almost_attained:
  assumes "infdist x X < a" "X ≠ {}"
  shows "∃y∈X. dist x y < a"
using assms using cInf_less_iff[of "(dist x)`X"] unfolding infdist_def by auto

lemma infdist_triangle_abs [mono_intros]:
  "¦infdist x A - infdist y A¦ ≤ dist x y"
by (metis (full_types) abs_diff_le_iff diff_le_eq dist_commute infdist_triangle)

text ‹The next lemma is missing in the library, contrary to its cousin \verb+continuous_infdist+.›

text ‹The infimum of the distance to a singleton set is simply the distance to the unique
member of the set.›

text ‹The closest point projection of $x$ on $A$. It is not unique, so we choose one point realizing the minimal
distance. And if there is no such point, then we use $x$, to make some statements true without any
assumption.›

definition proj_set::"'a::metric_space ⇒ 'a set ⇒ 'a set"
  where "proj_set x A = {y ∈ A. dist x y = infdist x A}"

definition distproj::"'a::metric_space ⇒ 'a set ⇒ 'a"
  where "distproj x A = (if proj_set x A ≠ {} then SOME y. y ∈ proj_set x A else x)"

lemma proj_setD:
  assumes "y ∈ proj_set x A"
  shows "y ∈ A" "dist x y = infdist x A"
using assms unfolding proj_set_def by auto

lemma proj_setI:
  assumes "y ∈ A" "dist x y ≤ infdist x A"
  shows "y ∈ proj_set x A"
using assms infdist_le[OF ‹y ∈ A›, of x] unfolding proj_set_def by auto

lemma proj_setI':
  assumes "y ∈ A" "⋀z. z ∈ A ⟹ dist x y ≤ dist x z"
  shows "y ∈ proj_set x A"
proof (rule proj_setI[OF ‹y ∈ A›])
  show "dist x y ≤ infdist x A"
    apply (subst infdist_notempty)
    using assms by (auto intro!: cInf_greatest)
qed

lemma distproj_in_proj_set:
  assumes "proj_set x A ≠ {}"
  shows "distproj x A ∈ proj_set x A"
        "distproj x A ∈ A"
        "dist x (distproj x A) = infdist x A"
proof -
  show "distproj x A ∈ proj_set x A"
    using assms unfolding distproj_def using some_in_eq by auto
  then show "distproj x A ∈ A" "dist x (distproj x A) = infdist x A"
    unfolding proj_set_def by auto
qed

lemma proj_set_nonempty_of_proper:
  assumes "proper A" "A ≠ {}"
  shows "proj_set x A ≠ {}"
proof -
  have "∃y. y ∈ A ∧ dist x y = infdist x A"
    using infdist_proper_attained[OF assms, of x] by auto
  then show "proj_set x A ≠ {}" unfolding proj_set_def by auto
qed

lemma distproj_self [simp]:
  assumes "x ∈ A"
  shows "proj_set x A = {x}"
        "distproj x A = x"
proof -
  show "proj_set x A = {x}"
    unfolding proj_set_def using assms by auto
  then show "distproj x A = x"
    unfolding distproj_def by auto
qed

lemma distproj_closure [simp]:
  assumes "x ∈ closure A"
  shows "distproj x A = x"
proof (cases "proj_set x A ≠ {}")
  case True
  show ?thesis
    using distproj_in_proj_set(3)[OF True] assms
    by (metis closure_empty dist_eq_0_iff distproj_self(2) in_closure_iff_infdist_zero)
next
  case False
  then show ?thesis unfolding distproj_def by auto
qed

lemma distproj_le:
  assumes "y ∈ A"
  shows "dist x (distproj x A) ≤ dist x y"
proof (cases "proj_set x A ≠ {}")
  case True
  show ?thesis using distproj_in_proj_set(3)[OF True] infdist_le[OF assms] by auto
next
  case False
  then show ?thesis unfolding distproj_def by auto
qed

lemma proj_set_dist_le:
  assumes "y ∈ A" "p ∈ proj_set x A"
  shows "dist x p ≤ dist x y"
  using assms infdist_le unfolding proj_set_def by auto

subsection ‹Material on ereal and ennreal›

text ‹We add the simp rules that we needed to make all computations become more or less automatic.›

lemma ereal_of_real_of_ereal_iff [simp]:
  "ereal(real_of_ereal x) = x ⟷ x ≠ ∞ ∧ x ≠ - ∞"
  "x = ereal(real_of_ereal x) ⟷ x ≠ ∞ ∧ x ≠ - ∞"
by (metis MInfty_neq_ereal(1) PInfty_neq_ereal(2) real_of_ereal.elims)+

declare ereal_inverse_eq_0 [simp]
declare ereal_0_gt_inverse [simp]
declare ereal_inverse_le_0_iff [simp]
declare ereal_divide_eq_0_iff [simp]
declare ereal_mult_le_0_iff [simp]
declare ereal_zero_le_0_iff [simp]
declare ereal_mult_less_0_iff [simp]
declare ereal_zero_less_0_iff [simp]
declare ereal_uminus_eq_reorder [simp]
declare ereal_minus_le_iff [simp]

lemma ereal_inverse_noteq_minus_infinity [simp]:
  "1/(x::ereal) ≠ -∞"
by (simp add: divide_ereal_def)

lemma ereal_inverse_positive_iff_nonneg_not_infinity [simp]:
  "0 < 1/(x::ereal) ⟷ (x ≥ 0 ∧ x ≠ ∞)"
by (cases x, auto simp add: one_ereal_def)

lemma ereal_inverse_negative_iff_nonpos_not_infinity' [simp]:
  "0 > inverse (x::ereal) ⟷ (x < 0 ∧ x ≠ -∞)"
by (cases x, auto simp add: one_ereal_def)

lemma ereal_divide_pos_iff [simp]:
  "0 < x/(y::ereal) ⟷ (y ≠ ∞ ∧ y ≠ -∞) ∧ ((x > 0 ∧ y > 0) ∨ (x < 0 ∧ y < 0) ∨ (y = 0 ∧ x > 0))"
unfolding divide_ereal_def by auto

lemma ereal_divide_neg_iff [simp]:
  "0 > x/(y::ereal) ⟷ (y ≠ ∞ ∧ y ≠ -∞) ∧ ((x > 0 ∧ y < 0) ∨ (x < 0 ∧ y > 0) ∨ (y = 0 ∧ x < 0))"
unfolding divide_ereal_def by auto

text ‹More additions to \verb+mono_intros+.›

lemma ereal_leq_imp_neg_leq [mono_intros]:
  fixes x y::ereal
  assumes "x ≤ y"
  shows "-y ≤ -x"
using assms by auto

lemma ereal_le_imp_neg_le [mono_intros]:
  fixes x y::ereal
  assumes "x < y"
  shows "-y < -x"
using assms by auto

declare ereal_mult_left_mono [mono_intros]
declare ereal_mult_right_mono [mono_intros]
declare ereal_mult_strict_right_mono [mono_intros]
declare ereal_mult_strict_left_mono [mono_intros]

text ‹Monotonicity of basic inclusions.›

lemma ennreal_mono':
  "mono ennreal"
by (simp add: ennreal_leI monoI)

lemma enn2ereal_mono':
  "mono enn2ereal"
by (simp add: less_eq_ennreal.rep_eq mono_def)

lemma e2ennreal_mono':
  "mono e2ennreal"
by (simp add: e2ennreal_mono mono_def)

lemma enn2ereal_mono [mono_intros]:
  assumes "x ≤ y"
  shows "enn2ereal x ≤ enn2ereal y"
using assms less_eq_ennreal.rep_eq by auto

lemma ereal_mono:
  "mono ereal"
unfolding mono_def by auto

lemma ereal_strict_mono:
  "strict_mono ereal"
unfolding strict_mono_def by auto

lemma ereal_mono2 [mono_intros]:
  assumes "x ≤ y"
  shows "ereal x ≤ ereal y"
by (simp add: assms)

lemma ereal_strict_mono2 [mono_intros]:
  assumes "x < y"
  shows "ereal x < ereal y"
using assms by auto

lemma enn2ereal_a_minus_b_plus_b [mono_intros]:
  "enn2ereal a ≤ enn2ereal (a - b) + enn2ereal b"
by (metis diff_add_self_ennreal less_eq_ennreal.rep_eq linear plus_ennreal.rep_eq)

text ‹The next lemma follows from the same assertion in ereals.›

lemma enn2ereal_strict_mono [mono_intros]:
  assumes "x < y"
  shows "enn2ereal x < enn2ereal y"
using assms less_ennreal.rep_eq by auto

declare ennreal_mult_strict_left_mono [mono_intros]
declare ennreal_mult_strict_right_mono [mono_intros]

lemma ennreal_ge_0 [mono_intros]:
  assumes "0 < x"
  shows "0 < ennreal x"
by (simp add: assms)


text ‹The next lemma is true and useful in ereal. Note that variants such as $a + b \leq c + d$
implies $a-d \leq c -b$ are not true -- take $a = c = \infty$ and $b = d = 0$...›

lemma ereal_minus_le_minus_plus [mono_intros]:
  fixes a b c::ereal
  assumes "a ≤ b + c"
  shows "-b ≤ -a + c"
  using assms apply (cases a, cases b, cases c, auto)
  using ereal_infty_less_eq2(2) ereal_plus_1(4) by fastforce

lemma tendsto_ennreal_0 [tendsto_intros]:
  assumes "(u ⤏ 0) F"
  shows "((λn. ennreal(u n)) ⤏ 0) F"
unfolding ennreal_0[symmetric] by (intro tendsto_intros assms)

lemma tendsto_ennreal_1 [tendsto_intros]:
  assumes "(u ⤏ 1) F"
  shows "((λn. ennreal(u n)) ⤏ 1) F"
unfolding ennreal_1[symmetric] by (intro tendsto_intros assms)

subsection ‹Miscellaneous›

lemma lim_ceiling_over_n [tendsto_intros]:
  assumes "(λn. u n/n) ⇢ l"
  shows "(λn. ceiling(u n)/n) ⇢ l"
proof (rule tendsto_sandwich[of "λn. u n/n" _ _ "λn. u n/n + 1/n"])
  show "∀⇩F n in sequentially. u n / real n ≤ real_of_int ⌈u n⌉ / real n"
    unfolding eventually_sequentially by (rule exI[of _ 1], auto simp add: divide_simps)
  show "∀⇩F n in sequentially. real_of_int ⌈u n⌉ / real n ≤ u n / real n + 1 / real n"
    unfolding eventually_sequentially by (rule exI[of _ 1], auto simp add: divide_simps)
  have "(λn. u n / real n + 1 / real n) ⇢ l + 0"
    by (intro tendsto_intros assms)
  then show "(λn. u n / real n + 1 / real n) ⇢ l" by auto
qed (simp add: assms)

subsubsection ‹Liminfs and Limsups›

text ‹More facts on liminfs and limsups›

lemma Limsup_obtain':
  fixes u::"'a ⇒ 'b::complete_linorder"
  assumes "Limsup F u > c" "eventually P F"
  shows "∃n. P n ∧ u n > c"
proof -
  have *: "(INF P∈{P. eventually P F}. SUP x∈{x. P x}. u x) > c" using assms by (simp add: Limsup_def)
  have **: "c < (SUP x∈{x. P x}. u x)" using less_INF_D[OF *, of P] assms by auto
  then show ?thesis by (simp add: less_SUP_iff)
qed

lemma limsup_obtain:
  fixes u::"nat ⇒ 'a :: complete_linorder"
  assumes "limsup u > c"
  shows "∃n ≥ N. u n > c"
using Limsup_obtain'[OF assms, of "λn. n ≥ N"] unfolding eventually_sequentially by auto

lemma Liminf_obtain':
  fixes u::"'a ⇒ 'b::complete_linorder"
  assumes "Liminf F u < c" "eventually P F"
  shows "∃n. P n ∧ u n < c"
proof -
  have *: "(SUP P∈{P. eventually P F}. INF x∈{x. P x}. u x) < c" using assms by (simp add: Liminf_def)
  have **: "(INF x∈{x. P x}. u x) < c" using SUP_lessD[OF *, of P] assms by auto
  then show ?thesis by (simp add: INF_less_iff)
qed

lemma liminf_obtain:
  fixes u::"nat ⇒ 'a :: complete_linorder"
  assumes "liminf u < c"
  shows "∃n ≥ N. u n < c"
using Liminf_obtain'[OF assms, of "λn. n ≥ N"] unfolding eventually_sequentially by auto

text ‹The Liminf of a minimum is the minimum of the Liminfs.›

lemma Liminf_min_eq_min_Liminf:
  fixes u v::"nat ⇒ 'a::complete_linorder"
  shows "Liminf F (λn. min (u n) (v n)) = min (Liminf F u) (Liminf F v)"
proof (rule order_antisym)
  show "Liminf F (λn. min (u n) (v n)) ≤ min (Liminf F u) (Liminf F v)"
    by (auto simp add: Liminf_mono)

  have "Liminf F (λn. min (u n) (v n)) > w" if H: "min (Liminf F u) (Liminf F v) > w" for w
  proof (cases "{w<..<min (Liminf F u) (Liminf F v)} = {}")
    case True
    have "eventually (λn. u n > w) F" "eventually (λn. v n > w) F"
      using H le_Liminf_iff by fastforce+
    then have "eventually (λn. min (u n) (v n) > w) F"
      apply auto using eventually_elim2 by fastforce
    moreover have "z > w ⟹ z ≥ min (Liminf F u) (Liminf F v)" for z
      using H True not_le_imp_less by fastforce
    ultimately have "eventually (λn. min (u n) (v n) ≥ min (Liminf F u) (Liminf F v)) F"
      by (simp add: eventually_mono)
    then have "min (Liminf F u) (Liminf F v) ≤ Liminf F (λn. min (u n) (v n))"
      by (metis Liminf_bounded)
    then show ?thesis using H less_le_trans by blast
  next
    case False
    then obtain z where "z ∈ {w<..<min (Liminf F u) (Liminf F v)}"
      by blast
    then have H: "w < z" "z < min (Liminf F u) (Liminf F v)"
      by auto
    then have "eventually (λn. u n > z) F" "eventually (λn. v n > z) F"
      using le_Liminf_iff by fastforce+
    then have "eventually (λn. min (u n) (v n) > z) F"
      apply auto using eventually_elim2 by fastforce
    then have "Liminf F (λn. min (u n) (v n)) ≥ z"
      by (simp add: Liminf_bounded eventually_mono less_imp_le)
    then show ?thesis using H(1)
      by auto
  qed
  then show "min (Liminf F u) (Liminf F v) ≤ Liminf F (λn. min (u n) (v n))"
    using not_le_imp_less by blast
qed

text ‹The Limsup of a maximum is the maximum of the Limsups.›

lemma Limsup_max_eq_max_Limsup:
  fixes u::"'a ⇒ 'b::complete_linorder"
  shows "Limsup F (λn. max (u n) (v n)) = max (Limsup F u) (Limsup F v)"
proof (rule order_antisym)
  show "max (Limsup F u) (Limsup F v) ≤ Limsup F (λn. max (u n) (v n))"
    by (auto intro: Limsup_mono)

  have "Limsup F (λn. max (u n) (v n)) < e" if "max (Limsup F u) (Limsup F v) < e" for e
  proof (cases "∃t. max (Limsup F u) (Limsup F v) < t ∧ t < e")
    case True
    then obtain t where t: "t < e" "max (Limsup F u) (Limsup F v) < t" by auto
    then have "Limsup F u < t" "Limsup F v < t" using that max_def by auto
    then have *: "eventually (λn. u n < t) F" "eventually (λn. v n < t) F"
      by (auto simp: Limsup_lessD)
    have "eventually (λn. max (u n) (v n) < t) F"
      using eventually_mono[OF eventually_conj[OF *]] by auto
    then have "Limsup F (λn. max (u n) (v n)) ≤ t"
      by (meson Limsup_obtain' not_le_imp_less order.asym)
    then show ?thesis
      using t by auto
  next
    case False
    have "Limsup F u < e" "Limsup F v < e" using that max_def by auto
    then have *: "eventually (λn. u n < e) F" "eventually (λn. v n < e) F"
      by (auto simp: Limsup_lessD)
    have "eventually (λn. max (u n) (v n) ≤ max (Limsup F u) (Limsup F v)) F"
      apply (rule eventually_mono[OF eventually_conj[OF *]]) using False not_le_imp_less by force
    then have "Limsup F (λn. max (u n) (v n)) ≤ max (Limsup F u) (Limsup F v)"
      by (meson Limsup_obtain' leD leI)
    then show ?thesis using that le_less_trans by blast
  qed
  then show "Limsup F (λn. max (u n) (v n)) ≤ max (Limsup F u) (Limsup F v)"
    using not_le_imp_less by blast
qed

subsubsection ‹Bounding the cardinality of a finite set›

text ‹A variation with real bounds.›

lemma finite_finite_subset_caract':
  fixes C::real
  assumes "⋀G. G ⊆ F ⟹ finite G ⟹ card G ≤ C"
  shows "finite F ∧ card F ≤ C"
by (meson assms finite_if_finite_subsets_card_bdd le_nat_floor order_refl)

text ‹To show that a set has cardinality at most one, it suffices to show that any two of its
elements coincide.›

lemma finite_at_most_singleton:
  assumes "⋀x y. x ∈ F ⟹ y ∈ F ⟹ x = y"
  shows "finite F ∧ card F ≤ 1"
proof (cases "F = {}")
  case True
  then show ?thesis by auto
next
  case False
  then obtain x where "x ∈ F" by auto
  then have "F = {x}" using assms by auto
  then show ?thesis by auto
qed

text ‹Bounded sets of integers are finite.›

lemma finite_real_int_interval [simp]:
  "finite (range real_of_int ∩ {a..b})"
proof -
  have "range real_of_int ∩ {a..b} ⊆ real_of_int`{floor a..ceiling b}"
    by (auto, metis atLeastAtMost_iff ceiling_mono ceiling_of_int floor_mono floor_of_int image_eqI)
  then show ?thesis using finite_subset by blast
qed

text ‹Well separated sets of real numbers are finite, with controlled cardinality.›

lemma separated_in_real_card_bound:
  assumes "T ⊆ {a..(b::real)}" "d > 0" "⋀x y. x ∈ T ⟹ y ∈ T ⟹ y > x ⟹ y ≥ x + d"
  shows "finite T" "card T ≤ nat (floor ((b-a)/d) + 1)"
proof -
  define f where "f = (λx. floor ((x-a) / d))"
  have "f`{a..b} ⊆ {0..floor ((b-a)/d)}"
    unfolding f_def using ‹d > 0› by (auto simp add: floor_mono frac_le)
  then have *: "f`T ⊆ {0..floor ((b-a)/d)}" using ‹T ⊆ {a..b}› by auto
  then have "finite (f`T)" by (rule finite_subset, auto)
  have "card (f`T) ≤ card {0..floor ((b-a)/d)}" apply (rule card_mono) using * by auto
  then have card_le: "card (f`T) ≤ nat (floor ((b-a)/d) + 1)" using card_atLeastAtMost_int by auto

  have *: "f x ≠ f y" if "y ≥ x + d" for x y
  proof -
    have "(y-a)/d ≥ (x-a)/d + 1" using ‹d > 0› that by (auto simp add: divide_simps)
    then show ?thesis unfolding f_def by linarith
  qed
  have "inj_on f T"
    unfolding inj_on_def using * assms(3) by (auto, metis not_less_iff_gr_or_eq)
  show "finite T"
    using ‹finite (f`T)› ‹inj_on f T› finite_image_iff by blast
  have "card T = card (f`T)"
    using ‹inj_on f T› by (simp add: card_image)
  then show "card T ≤ nat (floor ((b-a)/d) + 1)"
    using card_le by auto
qed


subsection ‹Manipulating finite ordered sets›

text ‹We will need below to construct finite sets of real numbers with good properties expressed
in terms of consecutive elements of the set. We introduce tools to manipulate such sets,
expressing in particular the next and the previous element of the set and controlling how they
evolve when one inserts a new element in the set. It works in fact in any linorder, and could
also prove useful to construct sets of integer numbers.

Manipulating the next and previous elements work well, except at the top (respectively bottom).
In our constructions, these will be fixed and called $b$ and $a$.›

text ‹Notations for the next and the previous elements.›

definition next_in::"'a set ⇒ 'a ⇒ ('a::linorder)"
  where "next_in A u = Min (A ∩ {u<..})"

definition prev_in::"'a set ⇒ 'a ⇒ ('a::linorder)"
  where "prev_in A u = Max (A ∩ {..<u})"

context
  fixes A::"('a::linorder) set" and a b::'a
  assumes A: "finite A" "A ⊆ {a..b}" "a ∈ A" "b ∈ A" "a < b"
begin

text ‹Basic properties of the next element, when one starts from an element different from top.›

lemma next_in_basics:
  assumes "u ∈ {a..<b}"
  shows "next_in A u ∈ A"
        "next_in A u > u"
        "A ∩ {u<..<next_in A u} = {}"
proof -
  have next_in_A: "next_in A u ∈ A ∩ {u<..}"
    unfolding next_in_def apply (rule Min_in)
    using assms ‹finite A› ‹b ∈ A› by auto
  then show "next_in A u ∈ A" "next_in A u > u" by auto
  show "A ∩ {u<..<next_in A u} = {}"
    unfolding next_in_def using A by (auto simp add: leD)
qed

lemma next_inI:
  assumes "u ∈ {a..<b}"
          "v ∈ A"
          "v > u"
          "{u<..<v} ∩ A = {}"
  shows "next_in A u = v"
using assms next_in_basics[OF ‹u ∈ {a..<b}›] by fastforce

text ‹Basic properties of the previous element, when one starts from an element different from
bottom.›

lemma prev_in_basics:
  assumes "u ∈ {a<..b}"
  shows "prev_in A u ∈ A"
        "prev_in A u < u"
        "A ∩ {prev_in A u<..<u} = {}"
proof -
  have prev_in_A: "prev_in A u ∈ A ∩ {..<u}"
    unfolding prev_in_def apply (rule Max_in)
    using assms ‹finite A› ‹a ∈ A› by auto
  then show "prev_in A u ∈ A" "prev_in A u < u" by auto
  show "A ∩ {prev_in A u<..<u} = {}"
    unfolding prev_in_def using A by (auto simp add: leD)
qed

lemma prev_inI:
  assumes "u ∈ {a<..b}"
          "v ∈ A"
          "v < u"
          "{v<..<u} ∩ A = {}"
  shows "prev_in A u = v"
using assms prev_in_basics[OF ‹u ∈ {a<..b}›]
by (meson disjoint_iff_not_equal greaterThanLessThan_iff less_linear)

text ‹The interval $[a,b]$ is covered by the intervals between the consecutive elements of $A$.›

lemma intervals_decomposition:
  "(⋃ U ∈ {{u..next_in A u} | u. u ∈ A - {b}}. U) = {a..b}"
proof
  show "(⋃U∈{{u..next_in A u} |u. u ∈ A - {b}}. U) ⊆ {a..b}"
    using ‹A ⊆ {a..b}› next_in_basics(1) apply auto apply fastforce
    by (metis ‹A ⊆ {a..b}› atLeastAtMost_iff eq_iff le_less_trans less_eq_real_def not_less subset_eq subset_iff_psubset_eq)

  have "x ∈ (⋃U∈{{u..next_in A u} |u. u ∈ A - {b}}. U)" if "x ∈ {a..b}" for x
  proof -
    consider "x = b" | "x ∈ A - {b}" | "x ∉ A" by blast
    then show ?thesis
    proof(cases)
      case 1
      define u where "u = prev_in A b"
      have "b ∈ {a<..b}" using ‹a < b› by simp
      have "u ∈ A - {b}" unfolding u_def using prev_in_basics[OF ‹b ∈ {a<..b}›] by simp
      then have "u ∈ {a..<b}" using ‹A ⊆ {a..b}› ‹a < b› by fastforce
      have "next_in A u = b"
        using prev_in_basics[OF ‹b ∈ {a<..b}›] next_in_basics[OF ‹u ∈ {a..<b}›] ‹A ⊆ {a..b}› unfolding u_def by force
      then have "x ∈ {u..next_in A u}" unfolding 1 using prev_in_basics[OF ‹b ∈ {a<..b}›] u_def by auto
      then show ?thesis using ‹u ∈ A - {b}› by auto
    next
      case 2
      then have "x ∈ {a..<b}" using ‹A ⊆ {a..b}› ‹a < b› by fastforce
      have "x ∈ {x.. next_in A x}" using next_in_basics[OF ‹x ∈ {a..<b}›] by auto
      then show ?thesis using 2 by auto
    next
      case 3
      then have "x ∈ {a<..b}" using that ‹a ∈ A› leI by fastforce
      define u where "u = prev_in A x"
      have "u ∈ A - {b}" unfolding u_def using prev_in_basics[OF ‹x ∈ {a<..b}›] that by auto
      then have "u ∈ {a..<b}" using ‹A ⊆ {a..b}› ‹a < b› by fastforce
      have "x ∈ {u..next_in A u}"
        using prev_in_basics[OF ‹x ∈ {a<..b}›] next_in_basics[OF ‹u ∈ {a..<b}›] unfolding u_def by auto
      then show ?thesis using ‹u ∈ A - {b}› by auto
    qed
  qed
  then show "{a..b} ⊆ (⋃U∈{{u..next_in A u} |u. u ∈ A - {b}}. U)" by auto
qed
end

text ‹If one inserts an additional element, then next and previous elements are not modified,
except at the location of the insertion.›

lemma next_in_insert:
  assumes A: "finite A" "A ⊆ {a..b}" "a ∈ A" "b ∈ A" "a < b"
      and "x ∈ {a..b} - A"
  shows "⋀u. u ∈ A - {b, prev_in A x} ⟹ next_in (insert x A) u = next_in A u"
        "next_in (insert x A) x = next_in A x"
        "next_in (insert x A) (prev_in A x) = x"
proof -
  define B where "B = insert x A"
  have B: "finite B" "B ⊆ {a..b}" "a ∈ B" "b ∈ B" "a < b"
    using assms unfolding B_def by auto
  have x: "x ∈ {a..<b}" "x ∈ {a<..b}" using assms leI by fastforce+
  show "next_in B x = next_in A x"
    unfolding B_def by (auto simp add: next_in_def)

  show "next_in B (prev_in A x) = x"
    apply (rule next_inI[OF B])
    unfolding B_def using prev_in_basics[OF A ‹x ∈ {a<..b}›] ‹A ⊆ {a..b}› x by auto

  fix u assume "u ∈ A - {b, prev_in A x}"
  then have "u ∈ {a..<b}" using assms by fastforce
  have "x ∉ {u<..<next_in A u}"
  proof (rule ccontr)
    assume "¬(x ∉ {u<..<next_in A u})"
    then have *: "x ∈ {u<..<next_in A u}" by auto
    have "prev_in A x = u"
      apply (rule prev_inI[OF A ‹x ∈ {a<..b}›])
      using ‹u ∈ A - {b, prev_in A x}› * next_in_basics[OF A ‹u ∈ {a..<b}›] apply auto
      by (meson disjoint_iff_not_equal greaterThanLessThan_iff less_trans)
    then show False using ‹u ∈ A - {b, prev_in A x}› by auto
  qed
  show "next_in B u = next_in A u"
    apply (rule next_inI[OF B ‹u ∈ {a..<b}›]) unfolding B_def
    using next_in_basics[OF A ‹u ∈ {a..<b}›] ‹x ∉ {u<..<next_in A u}› by auto
qed

text ‹If consecutive elements are enough separated, this implies a simple bound on the
cardinality of the set.›

lemma separated_in_real_card_bound2:
  fixes A::"real set"
  assumes A: "finite A" "A ⊆ {a..b}" "a ∈ A" "b ∈ A" "a < b"
      and B: "⋀u. u ∈ A - {b} ⟹ next_in A u ≥ u + d" "d > 0"
  shows "card A ≤ nat (floor ((b-a)/d) + 1)"
proof (rule separated_in_real_card_bound[OF ‹A ⊆ {a..b}› ‹d > 0›])
  fix x y assume "x ∈ A" "y ∈ A" "y > x"
  then have "x ∈ A - {b}" "x ∈ {a..<b}" using ‹A ⊆ {a..b}› by auto
  have "y ≥ next_in A x"
    using next_in_basics[OF A ‹x ∈ {a..<b}›] ‹y ∈ A› ‹y > x› by auto
  then show "y ≥ x + d" using B(1)[OF ‹x ∈ A - {b}›] by auto
qed


subsection ‹Well-orders›

text ‹In this subsection, we give additional lemmas on well-orders or cardinals or whatever,
that would well belong to the library, and will be needed below.›

lemma (in wo_rel) max2_underS [simp]:
  assumes "x ∈ underS z" "y ∈ underS z"
  shows "max2 x y ∈ underS z"
using assms max2_def by auto

lemma (in wo_rel) max2_underS' [simp]:
  assumes "x ∈ underS y"
  shows "max2 x y = y" "max2 y x = y"
apply (simp add: underS_E assms max2_def)
using assms max2_def ANTISYM antisym_def underS_E by fastforce

lemma (in wo_rel) max2_xx [simp]:
  "max2 x x = x"
using max2_def by auto

declare underS_notIn [simp]

text ‹The abbrevation $=o$ is used both in \verb+Set_Algebras+ and Cardinals.
We disable the one from \verb+Set_Algebras+.›

no_notation elt_set_eq (infix "=o" 50)

lemma regularCard_ordIso:
  assumes "Card_order r" "regularCard r" "s =o r"
  shows "regularCard s"
unfolding regularCard_def
proof (auto)
  fix K assume K: "K ⊆ Field s" "cofinal K s"
  obtain f where f: "bij_betw f (Field s) (Field r)" "embed s r f" using ‹s =o r› unfolding ordIso_def iso_def by auto
  have "f`K ⊆ Field r" using K(1) f(1) bij_betw_imp_surj_on by blast
  have "cofinal (f`K) r" unfolding cofinal_def
  proof
    fix a assume "a ∈ Field r"
    then obtain a' where a: "a' ∈ Field s" "f a' = a" using f
      by (metis bij_betw_imp_surj_on imageE)
    then obtain b' where b: "b' ∈ K" "a' ≠ b' ∧ (a', b') ∈ s"
      using ‹cofinal K s› unfolding cofinal_def by auto
    have P1: "f b' ∈ f`K" using b(1) by auto
    have "a' ≠ b'" "a' ∈ Field s" "b' ∈ Field s" using a(1) b K(1) by auto
    then have P2: "a ≠ f b'" unfolding a(2)[symmetric] using f(1) unfolding bij_betw_def inj_on_def by auto
    have "(a', b') ∈ s" using b by auto
    then have P3: "(a, f b') ∈ r" unfolding a(2)[symmetric] using f
      by (meson FieldI1 FieldI2 Card_order_ordIso[OF assms(1) assms(3)] card_order_on_def iso_defs(1) iso_iff2)
    show "∃b∈f ` K. a ≠ b ∧ (a, b) ∈ r"
      using P1 P2 P3 by blast
  qed
  then have "|f`K| =o r"
    using ‹regularCard r› ‹f`K ⊆ Field r› unfolding regularCard_def by auto
  moreover have "|f`K| =o |K|" using f(1) K(1)
    by (meson bij_betw_subset card_of_ordIsoI ordIso_symmetric)
  ultimately show "|K| =o s"
    using ‹s =o r› by (meson ordIso_symmetric ordIso_transitive)
qed

lemma AboveS_not_empty_in_regularCard:
  assumes "|S| <o r" "S ⊆ Field r"
  assumes r: "Card_order r" "regularCard r" "¬finite (Field r)"
  shows "AboveS r S ≠ {}"
proof -
  have "¬(cofinal S r)"
    using assms not_ordLess_ordIso unfolding regularCard_def by auto
  then obtain a where a: "a ∈ Field r" "∀b∈S. ¬(a ≠ b ∧ (a,b) ∈ r)"
    unfolding cofinal_def by auto
  have *: "a = b ∨ (b, a) ∈ r" if "b ∈ S" for b
  proof -
    have "a = b ∨ (a,b) ∉ r" using a that by auto
    then show ?thesis
      using ‹Card_order r› ‹a ∈ Field r› ‹b ∈ S› ‹S ⊆ Field r› unfolding card_order_on_def well_order_on_def linear_order_on_def total_on_def
      by auto
  qed
  obtain c where "c ∈ Field r" "c ≠ a" "(a, c) ∈ r"
    using a(1) r infinite_Card_order_limit by fastforce
  then have "c ∈ AboveS r S"
    unfolding AboveS_def apply simp using Card_order_trans[OF r(1)] by (metis *)
  then show ?thesis by auto
qed

lemma AboveS_not_empty_in_regularCard':
  assumes "|S| <o r" "f`S ⊆ Field r" "T ⊆ S"
  assumes r: "Card_order r" "regularCard r" "¬finite (Field r)"
  shows "AboveS r (f`T) ≠ {}"
proof -
  have "|f`T| ≤o |T|" by simp
  moreover have "|T| ≤o |S|" using ‹T ⊆ S› by simp
  ultimately have *: "|f`T| <o r" using ‹|S| <o r› by (meson ordLeq_ordLess_trans)
  show ?thesis using AboveS_not_empty_in_regularCard[OF * _ r] ‹T ⊆ S› ‹f`S ⊆ Field r› by auto
qed

lemma Well_order_extend:
assumes WELL: "well_order_on A r" and SUB: "A ⊆ B"
shows "∃r'. well_order_on B r' ∧ r ⊆ r'"
proof-
  have r: "Well_order r ∧ Field r = A" using WELL well_order_on_Well_order by blast
  let ?C = "B - A"
  obtain r'' where "well_order_on ?C r''" using well_order_on by blast
  then have r'': "Well_order r'' ∧ Field r'' = ?C"
    using well_order_on_Well_order by blast
  let ?r' = "r Osum r''"
  have "Field r Int Field r'' = {}" using r r'' by auto
  then have "r ≤o ?r'" using Osum_ordLeq[of r r''] r r'' by blast
  then have "Well_order ?r'" unfolding ordLeq_def by auto
  moreover have "Field ?r' = B" using r r'' SUB by (auto simp add: Field_Osum)
  ultimately have "well_order_on B ?r'" by auto
  moreover have "r ⊆ ?r'" by (simp add: Osum_def subrelI)
  ultimately show ?thesis by blast
qed

text ‹The next lemma shows that, if the range of a function is endowed with a wellorder,
then one can pull back this wellorder by the function, and then extend it in the fibers
of the function in order to keep the wellorder property.

The proof is done by taking an arbitrary family of wellorders on each of the fibers, and using
the lexicographic order: one has $x < y$ if $f x < f y$, or if $f x = f y$ and, in the corresponding
fiber of $f$, one has $x < y$.

To formalize it, it is however more efficient to use one single wellorder, and restrict it
to each fiber.›

lemma Well_order_pullback:
  assumes "Well_order r"
  shows "∃s. Well_order s ∧ Field s = UNIV ∧ (∀x y. (f x, f y) ∈ (r-Id) ⟶ (x, y) ∈ s)"
proof -
  obtain r2 where r2: "Well_order r2" "Field r2 = UNIV" "r ⊆ r2"
    using Well_order_extend[OF assms, of UNIV] well_order_on_Well_order by auto
  obtain s2 where s2: "Well_order s2" "Field s2 = (UNIV::'b set)"
    by (meson well_ordering)

  have r2s2:
    "⋀x y z. (x, y) ∈ s2 ⟹ (y, z) ∈ s2 ⟹ (x, z) ∈ s2"
    "⋀x. (x, x) ∈ s2"
    "⋀x y. (x, y) ∈ s2 ∨ (y, x) ∈ s2"
    "⋀x y. (x, y) ∈ s2 ⟹ (y, x) ∈ s2 ⟹ x = y"
    "⋀x y z. (x, y) ∈ r2 ⟹ (y, z) ∈ r2 ⟹ (x, z) ∈ r2"
    "⋀x. (x, x) ∈ r2"
    "⋀x y. (x, y) ∈ r2 ∨ (y, x) ∈ r2"
    "⋀x y. (x, y) ∈ r2 ⟹ (y, x) ∈ r2 ⟹ x = y"
    using r2 s2 unfolding well_order_on_def linear_order_on_def partial_order_on_def total_on_def preorder_on_def antisym_def refl_on_def trans_def
    by (metis UNIV_I)+

  define s where "s = {(x,y). (f x, f y) ∈ r2 ∧ (f x = f y ⟶ (x, y) ∈ s2)}"
  have "linear_order s"
  unfolding linear_order_on_def partial_order_on_def preorder_on_def
  proof (auto)
    show "total_on UNIV s"
      unfolding s_def apply (rule total_onI, auto) using r2s2 by metis+
    show "refl_on UNIV s"
      unfolding s_def apply (rule refl_onI, auto) using r2s2 by blast+
    show "trans s"
      unfolding s_def apply (rule transI, auto) using r2s2 by metis+
    show "antisym s"
      unfolding s_def apply (rule antisymI, auto) using r2s2 by metis+
  qed
  moreover have "wf (s - Id)"
  proof (rule wfI_min)
    fix x::'b and Q assume "x ∈ Q"
    obtain z' where z': "z' ∈ f`Q" "⋀y. (y, z') ∈ r2 - Id ⟶ y ∉ f`Q"
    proof (rule wfE_min[of "r2-Id" "f x" "f`Q"], auto)
      show "wf(r2-Id)" using ‹Well_order r2› unfolding well_order_on_def by auto
      show "f x ∈ f`Q" using ‹x ∈ Q› by auto
    qed
    define Q2 where "Q2 = Q ∩ f-`{z'}"
    obtain z where z: "z ∈ Q2" "⋀y. (y, z) ∈ s2 - Id ⟶ y ∉ Q2"
    proof (rule wfE_min'[of "s2-Id" "Q2"], auto)
      show "wf(s2-Id)" using ‹Well_order s2› unfolding well_order_on_def by auto
      assume "Q2 = {}"
      then show False unfolding Q2_def using ‹z' ∈ f`Q› by blast
    qed
    have "(y, z) ∈ (s-Id) ⟹ y ∉ Q" for y
      unfolding s_def using z' z Q2_def by auto
    then show "∃z∈Q. ∀y. (y, z) ∈ s - Id ⟶ y ∉ Q"
      using ‹z ∈ Q2› Q2_def by auto
  qed
  ultimately have "well_order_on UNIV s" unfolding well_order_on_def by simp
  moreover have "(f x, f y) ∈ (r-Id) ⟶ (x, y) ∈ s" for x y
    unfolding s_def using ‹r ⊆ r2› by auto
  ultimately show ?thesis using well_order_on_Well_order by metis
qed

end (*of theory Library_Complements*)